<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>The seL4 run-time | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">The seL4 run-time</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">















    <ul class="nav nav-sidebar">
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4/">seL4</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/l4v/">L4.verified</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/camkes/">CAmkES</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/capdl/">CapDL</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/elfloader/">Elfloader</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/buildsystem/">seL4 Buildsystem</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/user_libs/">user_libs</a>
        </li>
  
    
    

    
        <li class="active">
            <a class="" href="/projects/sel4runtime/">The seL4 run-time</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4webserver/">seL4webserver</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4-tutorials/">seL4 tutorials</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4bench/">sel4bench</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4test/">seL4Test</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/virtualization/">Virtualization</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/camkes-vm/">camkes-vm</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/dockerfiles/">Dockerfiles</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/docsite/">seL4 Documentation website</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4_tools/">seL4_tools</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/microkit/">Microkit</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/hardware_hacks/">Hardware Hacks</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/rust/">Rust</a>
        </li>
  
    </ul>


</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">
    
<!--
     Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)

     SPDX-License-Identifier: CC-BY-SA-4.0
-->

<h1 id="the-sel4-run-time">The seL4 Run-time</h1>

<p>This provides a minimal runtime for running a C or C-compatible process, 
i.e. one with a C-like <code class="language-plaintext highlighter-rouge">main</code>, in a minimal seL4 environment.</p>

<p>This runtime provides mechanisms for accessing everything a standard
process would expect to need at start and provides additional utilities
for delegating the creation of processes and threads.</p>

<h2 id="standard-processes">Standard Processes</h2>

<p>All processes (except for the root task) will use the entry-points
provided here as normal and require the <code class="language-plaintext highlighter-rouge">_start</code> entry-point provided in
the architecture-dependant <code class="language-plaintext highlighter-rouge">crt0.S</code>. This will then bootstrap into the
runtime entry-point <code class="language-plaintext highlighter-rouge">__sel4_start_c</code> which simply processes the stack to
find the argument, environment, and auxiliary vectors.</p>

<p>The found vectors, along with<code class="language-plaintext highlighter-rouge">main</code>, are passed into
<code class="language-plaintext highlighter-rouge">__sel4_start_main</code> which configures the runtime before starting
<code class="language-plaintext highlighter-rouge">main</code>.</p>

<h2 id="root-task">Root Task</h2>

<p>The root task requires an alternate entry-point <code class="language-plaintext highlighter-rouge">_sel4_start</code> which
assumes that the <code class="language-plaintext highlighter-rouge">seL4_BootInfo</code> argument has been passed to it and that
it has not been given a stack.</p>

<p>This entry-point moves onto a static 16 kilobyte stack before invoking
<code class="language-plaintext highlighter-rouge">__sel4_start_root</code>, which constructs the argument, environment, and
auxiliary vectors. It then passes the constructed vectors, along with
<code class="language-plaintext highlighter-rouge">main</code>, into <code class="language-plaintext highlighter-rouge">__sel4_start_main</code> which configures the runtime before
starting <code class="language-plaintext highlighter-rouge">main</code>.</p>

<h2 id="thread-local-storage-layout">Thread-local storage layout</h2>

<p>There are two standard layouts for thread local storage commonly used.
One where the TLS base address refers to the first address in memory of
the region and one where it refers to the address that immediately
follows the region. Intel’s x86_64 and ia32 architectures use the latter
method as it aligns with the segmentation view of memory presented by
the processor. Most other platforms use former method, where the TLS can
be said to be ‘above’ the thread pointer.</p>

<p>In order to store metadata for the current thread in the same memory
allocation as the TLS, the run-time utilises memory on the other side of
the thread pointer for it’s thread structure.</p>

<p><em>File included from <a href="https://github.com/sel4proj/sel4runtime/blob/master/README.md">github repo</a> <a href="https://github.com/sel4proj/sel4runtime/edit/master/README.md">edit</a></em></p>

<!--
     Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)

     SPDX-License-Identifier: CC-BY-SA-4.0
-->

<h2 id="c-run-time">C Run-time</h2>

<p>The standard convention for a static C run-time provides the following 3
files:</p>

<ul>
  <li><code class="language-plaintext highlighter-rouge">crt0.o</code>; This provides the <code class="language-plaintext highlighter-rouge">_start</code> symbol which is used as the entry
point into a C program.</li>
  <li><code class="language-plaintext highlighter-rouge">crti.o</code>; This provides the prologue to the <code class="language-plaintext highlighter-rouge">_init</code> and <code class="language-plaintext highlighter-rouge">_fini</code>
symbols. As it occurs in the linker arguments <em>before</em> other object
files, other object files may add function calls to the body of these
symbols.</li>
  <li><code class="language-plaintext highlighter-rouge">crtn.o</code>; This provides the epilogue to the <code class="language-plaintext highlighter-rouge">_init</code> and <code class="language-plaintext highlighter-rouge">_fini</code>
symbols and occurs in the linker arguments after all other object
files.</li>
</ul>

<h3 id="constructors-and-destructors">Constructors and Destructors.</h3>

<p>The C runtime provides a mechanism for providing functions to be
executed before and after <code class="language-plaintext highlighter-rouge">main</code> as constructors and destructors for
object files and global state.</p>

<p>There are two mechanisms that provide this as documented in the <a href="http://www.sco.com/developers/gabi/latest/ch4.sheader.html#special_sections">System
V ABI</a>.</p>

<p>The first is the aforementioned <code class="language-plaintext highlighter-rouge">_init</code> and <code class="language-plaintext highlighter-rouge">_fini</code> symbols. The second
is a set of regions called <code class="language-plaintext highlighter-rouge">.preinit_array</code>, <code class="language-plaintext highlighter-rouge">.init_array</code>, and
<code class="language-plaintext highlighter-rouge">.fini_array</code>. Each of these is simply a vector of void function
pointers to be executed.</p>

<p>The runtime must, before <code class="language-plaintext highlighter-rouge">main</code>, execute <code class="language-plaintext highlighter-rouge">_init</code>, all function pointers
in <code class="language-plaintext highlighter-rouge">.preinit_array</code>, then all function pointers in <code class="language-plaintext highlighter-rouge">.init_array</code>. The
runtime must also, at <code class="language-plaintext highlighter-rouge">exit</code>, execute all function pointers in
<code class="language-plaintext highlighter-rouge">.fini_array</code> in reverse, then execute <code class="language-plaintext highlighter-rouge">_fini</code>.</p>

<p>To assist in iterating through these arrays, GCC’s internal linker
script defines the symbols <code class="language-plaintext highlighter-rouge">__(preinit,init,fini)_array_(start,end)</code> in
the appropriate sections marking the first function in each and the end
of the array.</p>

<h3 id="the-_start-symbol">The <code class="language-plaintext highlighter-rouge">_start</code> Symbol</h3>

<p>Arguments to <code class="language-plaintext highlighter-rouge">_start</code> are on the stack for all platforms.
The top of the stack is structured as so:</p>

<ul>
  <li>argument count</li>
  <li>array of argument pointers</li>
  <li>an empty string</li>
  <li>array of environment pointers</li>
  <li>a null terminator</li>
  <li>array of auxiliary vector entries</li>
  <li>an ‘zero’ auxiliary vector</li>
  <li>unspecified data</li>
</ul>

<p>For simplicity, we simply pass a pointer to the stack to the C entry in
the runtime and dissasemble the stack there. The entry we use is as
follows:</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="kt">void</span> <span class="nf">__sel4_start_c</span><span class="p">(</span><span class="kt">void</span> <span class="o">*</span><span class="n">stack</span><span class="p">);</span>
</code></pre></div></div>

<p>NOTE: <code class="language-plaintext highlighter-rouge">__sel4_start_c</code> is a void function as it should call the
non-returning <code class="language-plaintext highlighter-rouge">_exit</code> symbol after calling <code class="language-plaintext highlighter-rouge">main</code>.</p>

<p><em>File included from <a href="https://github.com/sel4proj/sel4runtime/blob/master/crt/README.md">github repo</a> <a href="https://github.com/sel4proj/sel4runtime/edit/master/crt/README.md">edit</a></em></p>


  </div>







  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#standard-processes">Standard Processes</a></li>
<li class="toc-entry toc-h2"><a href="#root-task">Root Task</a></li>
<li class="toc-entry toc-h2"><a href="#thread-local-storage-layout">Thread-local storage layout</a></li>
<li class="toc-entry toc-h2"><a href="#c-run-time">C Run-time</a>
<ul>
<li class="toc-entry toc-h3"><a href="#constructors-and-destructors">Constructors and Destructors.</a></li>
<li class="toc-entry toc-h3"><a href="#the-_start-symbol">The _start Symbol</a></li>
</ul>
</li>
</ul>
</div>

  
  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
  
    <ul class="section-nav">
    	<h2> The seL4 run-time </h2> 
        <li>
          
          <a style=" font-weight: bold; " class="" href="/projects/sel4runtime/">
            Documentation homepage
          </a>
        </li>

















    
        <h3>Repositories</h3>
    
        <li>
          <a class="" href="https://github.com/seL4proj/sel4runtime">
            sel4runtime
          </a>
        </li>









  







    
        <h3>Recent Updates</h3>
    
        <li>
          <a style="" href="/updates/sel4runtime/11.0.x.html">
            seL4 11.0.x-compatible
          </a>
        </li>

    </ul>

</div>


</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Nov 30 09:25:37 2020 +1100 977ed44f17
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/sel4runtime/index.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/sel4runtime/index.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
